'''
Created on 2011-04-26

@author: kacper
'''
from dataStructs.formulaSet import Theory
from config.config import getAnyDatabase, testPath, getValidParseExamplesDirs
from dataStructs.Transform import cnf
from test.cnf_tests import testCNF
from logger.logger import instLog, instLogFun
from resolution.resolution import linearResolution

log = instLog("testTheory")
logFun = instLogFun(log)

if __name__ == '__main__':
    kb =  getValidParseExamplesDirs() + "/then3times.wn"
        
        
    print "knowledge base name ", kb
 
    th = Theory(kb)
    
    
    print "=== negations" 
    
    for x in th.theory:
        print x.negFormula().prt()
    
    print "=== assert ~~"
    for x in th.theory:
        print x.negFormula().negFormula().prt()
        print x.removeThen().prt()
        assert( x.negFormula().negFormula().pushNeg().prt() == x.removeThen().pushNeg().prt())

    print "push neg"
    for x in th.theory:
        print x.pushNeg().prt()


    print cnf(x).prt()
        
    print "convert to CNF"
    print th.convertToCNF()
    
    print "convert To resolution Form"
    print th.resolutionForm()
    
    
    
    print "carine"
    print th.carineFormRes()
    
    print "carine goal"
    
    trm = "a"
    
    print "is optymistic"
    print th.isOptymistic(trm)
  